
@manuscript{abadi+93,
title={{Types for the Scott Numerals}},
author={M. Abadi and L. Cardelli and G. Plotkin},
note="Unpublished, available from Abadi's web page",
year=1993,
pages={1--2}}                  
                  
@Book{CHS72,
title = {{Combinatory Logic}},
volume = "2",
author = "H. Curry and J. Hindley and J. Seldin",
year = "1972",
publisher = "North-Holland Publishing Company"}

                  @inproceedings{weirich+10,
  author = {Stephanie Weirich and Chris Casinghino},
  title = {{Arity-Generic Datatype-Generic Programming}},
  booktitle = {PLPV '10: Proceedings of the 4th Workshop on Programming Languages Meets Program Verification},
  year = {2010},
  editor="C. Flanagan and J.-C. Filli\^atre"                  
}
                  
@inproceedings{meyer+86,
 author = {Meyer, Albert R. and Reinhold, Mark B.},
 title = {"Type" is not a type},
 booktitle = {Proceedings of the 13th ACM SIGACT-SIGPLAN Symposium on Principles of programming languages (POPL)},
 year = {1986},
 pages = {287--295},
 publisher = {ACM},
} 
                  
@inproceedings{abel12,
  author    = {Andreas Abel},
  title     = {{Type-Based Termination, Inflationary Fixed-Points, and Mixed
               Inductive-Coinductive Types}},
  booktitle = {Proceedings 8th Workshop on Fixed Points in Computer Science (FICS)},
  year      = {2012},
  pages     = {1-11},
  editor    = {Dale Miller and
               Zolt{\'a}n {\'E}sik},
  series    = {EPTCS},
  volume    = {77}
}

@inproceedings{danielsson+10,
  author    = {Nils Anders Danielsson and
               Thorsten Altenkirch},
  title     = {{Subtyping, Declaratively}},
  pages     = {100-118},
  editor    = {Claude Bolduc and
               Jules Desharnais and
               B{\'e}chir Ktari},
  booktitle     = {Mathematics of Program Construction, 10th International
               Conference, MPC 2010, Qu{\'e}bec City, Canada, June 21-23,
               2010. Proceedings},
  year      = {2010},
}

@article{abel+11,
  author    = {Andreas Abel and
               Thorsten Altenkirch},
  title     = {{A Partial Type Checking Algorithm for Type: Type}},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {229},
  number    = {5},
  year      = {2011},
  pages     = {3-17}
}

@book{gtl90,
author = "J.-Y. Girard and Y. Lafont and P. Taylor",
year = 1990,
publisher = "Cambridge University Press",
title={{Proofs and Types}}}


@incollection {coquand+88,
   author = {Coquand, Thierry and Paulin, Christine},
   title = {Inductively defined types},
   booktitle = {COLOG-88},
   series = {Lecture Notes in Computer Science},
   editor = {Martin-Löf, Per and Mints, Grigori},
   publisher = {Springer},
   pages = {50-66},
   volume = {417},
}

                  @inproceedings{werner92,
author = {B. Werner},
title = {{A Normalization Proof for an Impredicative Type System with Large Elimination over Integers}},
booktitle="International Workshop on Types for Proofs and Programs (TYPES)",
year="1992",
editor={B. Nordstr\"om and K. Petersson and G. Plotkin},
note={The TYPES 1992 proceedings are available at \url{http://www.cse.chalmers.se/research/group/logic/Types/proc92.ps}.},
pages="341--357"}

@inproceedings{pfenning+89,
  author    = {Frank Pfenning and
               Christine Paulin-Mohring},
  title     = {Inductively Defined Types in the Calculus of Constructions},
  booktitle = {Mathematical Foundations of Programming Semantics},
  pages     = {209-228},
  editor    = {Michael G. Main and
               Austin Melton and
               Michael W. Mislove and
               David A. Schmidt},
  title     = {Mathematical Foundations of Programming Semantics (MFPS), 5th International
               Conference, Tulane University, New Orleans, Louisiana, USA,
               March 29 - April 1, 1989, Proceedings},
  year      = {1989},
}

                  @inproceedings{geuvers01,
  editor = "S. Abramsky",
  author    = {Herman Geuvers},
  title     = {Induction Is Not Derivable in Second Order Dependent Type
               Theory},
  booktitle = {Typed Lambda Calculi and Applications (TLCA)},
  year      = {2001},
  pages     = {166-181},
}

@INPROCEEDINGS{hickey96,
    author = {Jason J. Hickey},
    title = {Formal Objects in Type Theory Using Very Dependent Types},
    editor={Kim Bruce} ,                 
    booktitle = {In Foundations of Object Oriented Languages (FOOL) 3},
    year = {1996}
}

@inproceedings{miquel01,
  author    = {A. Miquel},
  title     = {{The Implicit Calculus of Constructions}},
  booktitle = {Typed Lambda Calculi and Applications},
  year      = {2001},
  pages     = {344-359},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2044},
}

@inproceedings{barras+08,
  author    = {B. Barras and
               B. Bernardo},
  title     = {{The Implicit Calculus of Constructions as a Programming
               Language with Dependent Types}},
  booktitle = {Foundations of Software Science and Computational Structures,
               11th International Conference, FOSSACS 2008},
  year      = {2008},
  pages     = {365-379},
  editor    = {Roberto M. Amadio},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4962},

}


@article{harper+91,
  author    = {Robert Harper and
               Robert Pollack},
  title     = {{Type Checking with Universes}},
  journal   = {Theor. Comput. Sci.},
  volume    = {89},
  number    = {1},
  year      = {1991},
  pages     = {107-136},
}
@inproceedings{coquand86,
    author = {Thierry Coquand},
    title = {{An Analysis of Girard's Paradox}},
    booktitle = {IEEE Symposium on Logic in Computer Science (LICS)},
    year = {1986},
    pages = {227--236}
}
                  
@dissertation{girard72,
author="Jean-Yves Girard",
title="Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur",
institution="Universit\'e Paris VII",
year="1972"}
 
@inproceedings{odersky+03,
  author    = {Martin Odersky and
               Vincent Cremet and
               Christine R{\"o}ckl and
               Matthias Zenger},
  title     = {{A Nominal Theory of Objects with Dependent Types}},
  booktitle = {17th European Conference on Object-Oriented Programming
                  (ECOOP)},
  year      = {2003},
  pages     = {201-224},
  editor    = {Luca Cardelli},
}

@TECHREPORT{crary99,
    author = {Karl Crary},
    title = {{Simple, Efficient Object Encoding using Intersection Types}},
    institution = {Carnegie Mellon University},
    number={CMU-CS-99-100},
    year = {1999}
}

@INPROCEEDINGS{abadi+94,
    author = {Martín Abadi and Luca Cardelli},
    title = {{A Theory of Primitive Objects - Second-Order Systems}},
    booktitle = {European Symposium on Programming (ESOP)},
    year = {1994},
    pages = {1--25},
    publisher = {Springer-Verlag}
}

@article{altenkirch+10,
  author = 	 {Thorsten Altenkirch and Nils Anders Danielsson and Andres L\"oh and Nicolas Oury},
  title = 	 {{$\Pi$}{$\Sigma$}: Dependent Types Without the Sugar},
  journal={Functional and Logic Programming},
  pages={40--55},
  year={2010},
  publisher={Springer}
}


@inproceedings{chapman+10,
 author = {Chapman, James and Dagand, Pierre-\'{E}variste and McBride, Conor and Morris, Peter},
 title = {The gentle art of levitation},
 booktitle = {{Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP)}},
 year = {2010},
 pages = {3--14},
 publisher = {ACM},
}                   

@TECHREPORT{cardelli86,
    author = {Luca Cardelli},
    title = {{A Polymorphic Lambda-calculus with Type:Type}},
    institution = {Digital Equipment Corporation},
    year = {1986}
}
                  
@article{coq88,
 author = {T. Coquand and G. Huet},
 title = {{The Calculus of Constructions}},
 journal = {Information and Computation},
 volume = {76},
 number = {2-3},
 year = {1988},
 pages = "95--120"}

@inproceedings{sjoberg+10,
  author    = {Vilhelm Sj{\"o}berg and
               Aaron Stump},
  title     = {{Equality, Quasi-Implicit Products, and Large Eliminations}},
  editor    = {Elaine Pimentel and
               Betti Venneri and
               Joe Wells},
  title     = {Proceedings Fifth Workshop on Intersection Types and Related
               Systems (ITRS)},
  year      = {2010},
  pages     = {90-100},
  series    = {EPTCS},
  volume    = {45},
}

@inproceedings{sjoberg+12,
  author = {Vilhelm Sj\"oberg and Chris Casinghino and Ki Yung Ahn and
            Nathan Collins and Harley D. Eades III and Peng Fu
            and Garrin Kimmell and Tim Sheard and Aaron Stump
            and Stephanie Weirich},
  title = {{Irrelevance, Heterogenous Equality, and Call-by-value Dependent Type Systems}},
  booktitle = {Mathematically Structured Functional Programming (MSFP) '12},
  year = 2012,
}
                  @inproceedings{ccasin:msfp12,
  author = {Chris Casinghino and Vilhelm Sj\"{o}berg and Stephanie Weirich},
  title = {{Step-Indexed Normalization for a Language with General Recursion}},
  booktitle = {Mathematically Structured Functional Programming (MSFP) '12},
  year = 2012,
}

@inproceedings{kimmell+12,
  author = {Garrin Kimmell and Aaron Stump and Harley D. Eades III and 
                 Peng Fu and Tim Sheard and Stephanie Weirich and Chris Casinghino
                 and Vilhelm Sj\"oberg and Nathan Collins and Ki Yung Ahn},
  title = {{Equational Reasoning about Programs with General Recursion and Call-by-value Semantics}},
  booktitle = {Programming Languages meets Program Verification (PLPV) '12},
  year = 2012,
  editor="Koen Claessen and Nikhil Swamy"
}

@article{barthe+97,
  author    = {Gilles Barthe and
               John Hatcliff and
               Morten Heine S{\o}rensen},
  title     = {A notion of classical pure type system},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {6},
  year      = {1997},
  pages     = {4-59},
}

                  @inproceedings{Parigot:1992,
	Booktitle = {Logic, Programming, and Automated Reasoning (LPAR)},
	Editor = {Voronkov, Andrei},
	Pages = {190-201},
	Series = {Lecture Notes in Computer Science},
	Title = {Lambda-Mu-Calculus: An algorithmic interpretation of classical natural deduction},
	Volume = {624},
	Year = {1992},
}

@inproceedings{Rehof:1994,
	Author = {Rehof, Jakob and S{\o}rensen, Morten Heine},
	Booktitle = {Proceedings of the International Conference on Theoretical Aspects of Computer Software (TACS)},
	Numpages = {27},
	Pages = {516--542},
	Publisher = {Springer-Verlag},
	Title = {{The LambdaDelta-calculus}},
	Year = {1994},
}

@article{McBride:04:view,
  author    = {Conor McBride and
               James McKinna},
  title     = {The view from the left},
  journal   = {J. Funct. Program.},
  volume    = {14},
  number    = {1},
  year      = {2004},
  pages     = {69-111},
  ee        = {http://dx.doi.org/10.1017/S0956796803004829},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}